T:Type, eq:EqDecider(T), es:event_system{i:l}, x:Id, e:{e:es-E(es)| es-dtype(es; loc(e); x; T)} .
(x changed before e)  sqequal(loc((last change to x before e)); loc(e)) 

latex

Definitions

t  T, x:A. B(x), loc(e), es-dtype(es; i; x; T), x:AB(x), P  Q, (last change to x before e), x:A  B(x), P  Q, P  Q, b, void, False, A, es-locl(es; e; e'), {x:A| B(x)} , Type, EqDecider(T), event_system{i:l}, atom{$n:n}, Id, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , A c B, @e(xv), e(e1,e2].P(e), <a, b>, s = t, es-E(es), x changed before e, guard(T), sq_type(T), sqequal(s; t)

Lemmas

Id sq, assert wf, changed wf, es-E wf, Id wf, event system wf, deq wf, last-change-property, es-loc-pred, es-locl-iff, last-change wf, es-dtype wf, es-loc wf